i:Id, L:(IdLnk List), k:Knd. @i: k sends only links in L  Dsys 

latex

Definitions	Id, t  T, IdLnk, type List, Knd, , x:A. B(x), k sends only on links in L, MsgA, IdDeq, eqof(d), f(a), if b then t else f fi , x.A(x), @i: k sends only links in L, Dsys
Lemmas	ifthenelse wf, eqof wf, id-deq wf, msga wf, ma-single-bframe wf, ma-empty wf, Knd wf, IdLnk wf, Id wf